\section{Массивы}

\begin{itemize}
  \item На уровне выражений:
     \begin{enumerate}
        \item \llang{\{$e_1$, $e_2$,$\dots$,$e_k$\}}, где $e_i$ --- выражения;
        \item \llang{$e_1$[$e_2$]}, где $e_i$ --- выражения.
     \end{enumerate}

  \item На уровне операторов: \llang{$e_1$[$e_2$]:=$e_3$}, где $e_i$ --- выражения.
\end{itemize}

Модификация семантики для выражений:

\begin{itemize}
  \item Множество значений: ${\cal V}=\ZZ\cup(\NN\to {\cal V})$;
  \item Состояния: $S=X\to{\cal V}$;
  \item Подстановка в массив: 

           $$
             v[i\gets y]=\lambda j.\left\{
                                      \begin{array}{rcl}
                                         y&,&j=i\\
                                         v\;j&,&\mbox{иначе}
                                      \end{array}
                                    \right.,\;v\in\NN\to{\cal V},\;i\in dom(v)
           $$
\end{itemize}

Семантика выражений:

$$
\sembr{\bullet}:{\cal E}\to(S\to{\cal V})
$$

Все правила сохраняются при условии, что $\sembr{A}\in\ZZ$ для подвыражения $A$.

Новые правила:

$$
\sembr{\llang{\{$e_1$, $e_2$, $\dots$, $e_k$\}}}=\lambda s.\lambda i.\left\{
                                                                       \begin{array}{rcl}
                                                                          \sembr{e_i}\; s&,&i\in[1\dots k]\\
                                                                          \mbox{не определено}&,&\mbox{иначе}
                                                                       \end{array}
                                                                    \right.
$$

$$
\sembr{\llang{$e_1$[$e_2$]}}=\lambda s.\left\{
                                         \begin{array}{rcl}
                                            (\sembr{e_1}\;s)\;(\sembr{e_2}\;s)&,&\sembr{e_1}\;s\in\NN\to{\cal V},\;\sembr{e_2}\;s\in dom(\sembr{e_1}\;s)\\
                                            \mbox{не определено}&,&\mbox{иначе}
                                         \end{array}
                                      \right.
$$

Правило для нового оператора:

$$
\trans{\inbr{s,i,o}}{\llang{$e_1$[$e_2$]:=$e_3$}}{\inbr{update(e_1,\sembr{e_2}\;s,\sembr{e_3}\;s,s),i,o}}
$$

где преобразование $update$ определено следующим образом:

$$
update(x,i,y,s)=s[x\gets(\sembr{x}\;s)[i\gets y]]
$$

$$
update(\llang{$e_1$[$e_2$]},i,y,s)=update(e_1,\sembr{e_2}\;s,(\sembr{\llang{$e_1$[$e_2$]}}\;s)[i\gets y],s)
$$

$$
update(\llang{\{$e_1$, $e_2$, $\dots$, $e_k$\}},i,y,s)=assign(e_i,y,s),\;i\in[1..k]
$$

$$
assign(x,y,s)=s[x\gets y]
$$

$$
assign(\llang{$e_1$[$e_2$]},y,s)=update(e_1,\sembr{e_2}\;s,y,s)
$$

